\begin{tabbing}
update{-}antecedent\=\{i:l\}\+
\\[0ex](${\it es}$; ${\it Cmd}$; ${\it Sys}$; ${\it Config}$; $u$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=($\forall$$e$:\{$e$:es{-}E{-}interface(${\it es}$;${\it Sys}$)$\mid$ $\uparrow$csupdate?(${\it Sys}$($e$))\} . es{-}causl(${\it es}$; ($u$($e$)); $e$))\+
\\[0ex]\& (\=$\forall$$e$:\{$e$:es{-}E{-}interface(${\it es}$;${\it Sys}$)$\mid$ $\uparrow$csupdate?(${\it Sys}$($e$))\} .\+
\\[0ex](\=($\uparrow$(($u$($e$)) $\in_{b}$ ${\it Sys}$))\+
\\[0ex]$\Rightarrow$ \=(valid{-}sys(${\it es}$;${\it Config}$;${\it Sys}$;$u$($e$))\+
\\[0ex]\& csupdate{-}cmds(${\it Sys}$($e$)) = sys{-}cmds(${\it Sys}$($u$($e$))) $\in$ (${\it Cmd}$ List)))
\-\-\\[0ex]\& (\=($\uparrow$(($u$($e$)) $\in_{b}$ ${\it Config}$))\+
\\[0ex]$\Rightarrow$ \=(($\uparrow$ccsucc?(${\it Config}$($u$($e$))))\+
\\[0ex]\& ccsucc{-}id(${\it Config}$($u$($e$))) = es{-}loc(${\it es}$; $e$) $\in$ Id
\\[0ex]\& let \=$n$\= = ccsucc{-}num(${\it Config}$($u$($e$))) in\+\+
\\[0ex]($n$ $<$ $\parallel$cmd{-}history\=\{i:l\}\+
\\[0ex](${\it es}$; ${\it Config}$; ${\it Cmd}$; ${\it Sys}$; ($u$($e$)))$\parallel$)
\-\-\\[0ex]\& \=csupdate{-}cmds(${\it Sys}$($e$))\+
\\[0ex]=
\\[0ex]nth\_tl($n$;cmd{-}history\{i:l\}(${\it es}$; ${\it Config}$; ${\it Cmd}$; ${\it Sys}$; ($u$($e$))))
\\[0ex]$\in$ (${\it Cmd}$ List))))
\-\-\-\-\-\\[0ex]\& (\=$\forall$\=$e_{1}$:\{$e$:es{-}E{-}interface(${\it es}$;${\it Sys}$)$\mid$ $\uparrow$csupdate?(${\it Sys}$($e$))\} ,\+\+
\\[0ex]$e_{2}$:\{$e$:es{-}E{-}interface(${\it es}$;${\it Sys}$)$\mid$ $\uparrow$csupdate?(${\it Sys}$($e$))\} .
\-\\[0ex]es{-}locl(${\it es}$; ($u$($e_{1}$)); ($u$($e_{2}$)))
\\[0ex]$\Rightarrow$ (es{-}loc(${\it es}$; $e_{1}$) = es{-}loc(${\it es}$; $e_{2}$) $\in$ Id)
\\[0ex]$\Rightarrow$ es{-}locl(${\it es}$; $e_{1}$; $e_{2}$))
\-\\[0ex]\& (\=$\forall$$e$:\{$e$:es{-}E{-}interface(${\it es}$;${\it Sys}$)$\mid$ $\uparrow$csupdate?(${\it Sys}$($e$))\} , $s$:es{-}E(${\it es}$).\+
\\[0ex]es{-}locl(${\it es}$; $s$; ($u$($e$)))
\\[0ex]$\Rightarrow$ \=((($\uparrow$($s$ $\in_{b}$ ${\it Sys}$)) \& valid{-}sys(${\it es}$;${\it Config}$;${\it Sys}$;$s$))\+
\\[0ex]$\vee$ (($\uparrow$($s$ $\in_{b}$ ${\it Config}$)) \& ($\uparrow$ccsucc?(${\it Config}$($s$)))))
\-\\[0ex]$\Rightarrow$ ($\exists$${\it e'}$:\{$e$:es{-}E{-}interface(${\it es}$;${\it Sys}$)$\mid$ $\uparrow$csupdate?(${\it Sys}$($e$))\} . ($u$(${\it e'}$) = $s$ $\in$ es{-}E(${\it es}$))))
\-\-
\end{tabbing}